Nuprl Lemma : deq-member_wf
11,40
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
L
:(
A
List),
x
:
A
. deq-member(
eq
;
x
;
L
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
deq-member(
eq
;
x
;
L
)
Lemmas
reduce
wf
,
bool
wf
,
bor
wf
,
eqof
wf
,
bfalse
wf
,
deq
wf
origin
A:Type, eq:EqDecider(A), L:(A List), x:A. deq-member(eq; x; L) 
A:Type, eq:EqDecider(A), L:(A List), x:A. deq-member(eq; x; L) x:A. B(x) T